Error

Whereas Identity does nothing in a fairly pleasant sort of way, Error does nothing in a particularly brutal and harsh fashion. Mathematically, Error is the function that destroys everything else in front of it. It is often written as ⊥.

#math87#
Error~x = Error  

In practice, destroying the entire document when we hit one error is a bit much, so we'll just print out an error message. The user can carry on past an error at their own risk, as the code will no longer be formally verified.
 
Maybe this function ought to return a more useful error message ...